Library cross_point

Require Export PointsType.
Require Import incidence.
Require Import TrianglesDefs.

Open Scope R_scope.

Section Triangle.

Context `{M:triangle_theory}.

Definition cross_point P U :=
 match P,U with
  cTriple p q r, cTriple u v w ⇒
  cTriple (p×u*(r×v + q×w)) (q×v*(p×w + r×u)) (r×w*(q×u + p×v))
 end.

Definition is_cross_point P Q R := eq_points P (cross_point Q R).

Lemma cross_point_property :
 ∀ P U,
  match cevian_triangle P, cevian_triangle U with
    (A',B',C'),(A'',B'',C'') ⇒ is_perspector (cross_point P U) (A',B',C') (inter (line pointA A'') (line B' C'),
                                                                             inter (line pointB B'') (line A' C'),
                                                                             inter (line pointC C'') (line A' B'))
  end.
Proof.
intros.
destruct P.
destruct U.
simpl.
unfold col;simpl.
repeat split;ring.
Qed.

End Triangle.